import net.sf.javabdd.BDD;
import net.sf.javabdd.BDDFactory;

/**
 * This class implements the logic behind the BDD for the n-queens problem
 * You should implement all the missing methods
 * 
 * @author Stavros Amanatidis
 *
 */


public class QueensLogic {
	
	private transient int[][] board;
	private transient int[][] boardIDs;
	private transient BDD bdd;
	private transient BDDFactory fac;

	public void initializeGame(final int size) {
		this.board = new int[size][size];
		boardIDs = new int[size][size];
		for (int row = 0, count = 0; row < boardIDs.length; row++) {
			for (int col = 0; col < boardIDs[1].length; col++) {
				boardIDs[row][col] = count++;     		
			}
		}
		final BDDCreator cre = new BDDCreator(board, boardIDs);
		bdd = cre.initializeBDD();
		fac = bdd.getFactory();
	}


	public int[][] getGameBoard() {
		
		return board;
	}

	public boolean insertQueen(final int row, final int col) {

		if (board[row][col] == -1 || board[row][col] == 1) {
			return true;
		}
		
		board[row][col] = 1;
		restrictVar(row, col); 
		updateBoard();
		return true;
	}
	

	private void restrictVar(int row, int col){
		bdd = bdd.restrict(fac.ithVar(boardIDs[row][col]));
	}
	
	private boolean unsatisfiable(int row, int col){
		return bdd.restrict(fac.ithVar(boardIDs[row][col])).isZero();
	}
	
	private boolean certain(int row, int col){
		return bdd.restrict(fac.nithVar(boardIDs[row][col])).isZero();
	}
	
	private void updateBoard(){
		for (int row = 0; row < board.length; row++) {
			for (int col = 0; col < board[1].length; col++) {
				if (board[row][col] == 0){
					if (unsatisfiable(row, col)){
						board[row][col] = -1;
						bdd = bdd.restrict(fac.nithVar(boardIDs[row][col]));
					}
					if (certain(row, col)) insertQueen(row,col);
				}
			}
		}
	}

}
